(include-book "../src/acl2/wolfram-code-utils")
(include-book "../src/acl2/grid")
(include-book "generators/grid-data-generator")
(include-book "testing" :dir :teachpacks)

;;Sanity check for wolfram code parser
(check-expect (parse-wolfram-code 141) 
    (list t nil t t nil nil nil t))


;;Test that ints->bools turns 0 into nil
;;and everything else into t
(defproperty ints->bools-as-expected
	(some-ints :value (cons (random-integer) (random-list-of (random-integer)))
	 idx :value (random-between 0 (1- (len some-ints)))
	 idx-int-val :value (nth idx some-ints)
	 expected-val :value (not (equal idx-int-val 0)))
	(equal (nth idx (ints->bools* some-ints)) expected-val))

;;Test that get-situation-number-explicit, which takes each of the neighbors
;;rather than the entire grid, works like get-situation-numbers
(defproperty get-situation-number-general-case-equals-explicit
	(a-grid :value (random-elementary-grid 15 1/2)
     pos :value (random-integer)
     left-neighbor-pos :value (1- pos)
     right-neighbor-pos :value (1+ pos)
     left-neighbor-alive :value (elementary-grid-get a-grid left-neighbor-pos)
     me-alive :value (elementary-grid-get a-grid pos)
     right-neighbor-alive :value (elementary-grid-get a-grid right-neighbor-pos))
    (equal (get-situation-number-explicit left-neighbor-alive me-alive right-neighbor-alive)
    	(get-situation-number a-grid pos)))

;;Now that we verified the two forms are equivalent,
;;test that the explicit version performs as advertised
;;(because it's easier to test)
;;As described in wolfram-code-utils,
;;   situation-number =
;;		1 if the right cell is alive + 
;;      2 if the middle cell is alive +
;;      4 if the left cell is alive
(defproperty get-situation-number-exp-performs-as-designed
	(lpos-alive :value (random-bool)
	 me-alive :value (random-bool)
	 rpos-alive :value (random-bool)
	 expected-value :value (+ (if rpos-alive 1 0)
	 						  (if me-alive 2 0)
 						  	  (if lpos-alive 4 0)))
	(equal expected-value (get-situation-number-explicit lpos-alive me-alive rpos-alive)))


;;Helper method:
;;Given a list of unique elements uniques, return true
;;iff each member of uniques appears in maybe-repeats
;;1 or more times, and no members of maybe-repeats
;;do not appear in uniques.
(defun has-same-members-with-poss-repeats (uniques maybe-repeats)
	(if (endp uniques)
		(not maybe-repeats)
		(if (member-equal (car uniques) maybe-repeats)
			(has-same-members-with-poss-repeats
				(cdr uniques)
				(remove-equal (car uniques) maybe-repeats))
			nil)))


;;Test that flattening an elementary grid returns only the set
;;cells
(defproperty flattening-elementary-grid-returns-expected-values
	(some-ints :value (random-list-of (random-integer))
	 ints-grid :value (elementary-grid-set-multiple
	 					(empty-elementary-grid)
	 					some-ints t))
	(has-same-members-with-poss-repeats
		(flatten-elementary-grid ints-grid) some-ints))
